Code and Notes (Week 3 Wednesday)

module W3a where

import Test.QuickCheck


expo :: Monoid a => a -> Integer -> a
expo _ 0 = mempty
expo x n = x `mappend` expo x (n-1)

newtype Product = Product Integer deriving (Show,Eq)

instance Semigroup Product where
  Product x <> Product y = Product(x*y)

instance Monoid Product where
  mempty = Product 1
  mappend = (<>)

fexpo :: Monoid a => a -> Integer -> a
fexpo _ 0 = mempty
fexpo x n
  | even n = y `mappend` y
  | otherwise = x `mappend` fexpo x (n-1) where
      y = fexpo x (n `div` 2)

instance Arbitrary Product where
  -- the generator that always generates 0
  arbitrary = Product <$> arbitrary

fexpo_prop1 :: Product -> Integer -> Property
fexpo_prop1 p n =
  n >= 0 ==> expo p n == fexpo p n

fexpo_prop_gen :: (Eq a, Monoid a) => a -> Integer -> Bool
fexpo_prop_gen p n =
  --n >= 0 ==>
  expo p n == fexpo p n

-- :set +s
-- turn on statistics
-- :unset +s
-- turn off statistics

{-  Here's an equation:

        x - x = 0

    in Haskell, the above is always valid
    no matter what expression x is.

    In C, you can find x:s such that the above
    is *invalid*

       getChar() - getChar() /= 0

 -}

{- Q: What did I mean by the reverse thing?

   A: <TODO>
 -}

myreverse :: [a] -> [a]
myreverse [] = []
myreverse(x:xs) = myreverse xs ++ [x]

-- myreverse(myreverse xs) == xs

{- But the *language* doesn't guarantee
   that any possible implementation of
   the type signature of reverse
   is an involution
 -}

myfakereverse :: [a] -> [a]
myfakereverse _ = []

{- A *functional correctness specification*
   is a set of properties of a program.

   In particular: it's a set of properties about
    the input/output behaviour of a program,
    not about e.g. runtime

   Functional specification:
   - "the program always return an odd number"

   Non-functional specification:
   - "the program should terminate within 10 years"
 -}

{- Unit testing (oversimplified)

   - write a bunch of test cases
     to test the components of a larger program
     in isolation
 -}
unit_test_reverse =
  (myreverse(myreverse ([]::[Int])) == []) &&
  (myreverse(myreverse [1]) == [1]) &&
  (myreverse(myreverse [1,2]) == [1,2])

{- In property-based testing.
   Instead of specifying individual test cases,
   specify the *property* that we want to test.

   Once you've specified the property,
   run the property on many random inputs.
 -}

property_reverse :: [Int] -> Bool
property_reverse xs =
  myreverse(myreverse xs) == xs


-- reverse(xs ++ ys) = reverse ys ++ reverse xs
property2_reverse :: [Int] -> [Int] -> Bool
property2_reverse xs ys =
  myreverse(xs ++ ys) == myreverse ys ++ myreverse xs